
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Common.Utils.PrintTypedData</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Common.Utils.PrintTypedData" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Common.Utils.PrintTypedData</h1>
<div class="coq">
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.Ascii.html">Ascii</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html">List</a></span>.<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html">ErgoSpec.Backend.ErgoBackend</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Misc.html">ErgoSpec.Common.Utils.Misc</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html">ErgoSpec.Common.Utils.Result</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html">ErgoSpec.Common.Utils.Provenance</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html">ErgoSpec.Common.Utils.NamespaceContext</a></span>.<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id">JsAst.JsNumber</span>. <br/>
<br/>
<span class="kwd">Local</span> <span class="kwd">Open</span> <span class="kwd">Scope</span> <span class="id">string</span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="PrintTypedData">PrintTypedData</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="print_brand">print_brand</a></span> (<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) (<span class="id">b</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Misc.html#get_local_part">get_local_part</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#b">b</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; "~" ++ <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#b">b</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">local_name</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#resolve_type_name">resolve_type_name</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_current_in_scope">namespace_ctxt_current_in_scope</a></span>) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>,<span class="id">local_name</span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">resolved_b</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id">resolved_b</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#b">b</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">local_name</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"~" ++ <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#b">b</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">_</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"~" ++ <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#b">b</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="PrintTypedData.Data">Data</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Context</span> {<span class="id">br</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Brands.BrandRelation.html#brand_relation">brand_relation</a></span>}.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="unpack_output">unpack_output</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">out</span> : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> (<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span> * <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#out">out</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dleft">dleft</a></span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#drec">drec</a></span> (("<span class="id">response</span>", <span class="id">response</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::("<span class="id">state</span>", <span class="id">state</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::("<span class="id">emit</span>", <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dcoll">dcoll</a></span> <span class="id">emits</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>))) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">response</span>, <span class="id">emits</span>, <span class="id">state</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">_</span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="fmt_nl">fmt_nl</a></span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#String">String.String</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.Ascii.html#ascii_of_N">ascii_of_N</a></span> 10) <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#EmptyString">EmptyString</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="fmt_dq">fmt_dq</a></span> := """".<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="string_of_data">string_of_data</a></span> (<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) (<span class="id">d</span> : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">jsonify</span> := <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoData.data_to_json_string">ErgoData.data_to_json_string</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#fmt_dq">fmt_dq</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">string_of_rec</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>) -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">fun</span> <span class="id">rec</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;("{"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#concat">String.concat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;", "<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">map</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">item</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#item">item</a></span>) ++ ": " ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_data">string_of_data</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#item">item</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#rec">rec</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "}") <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#d">d</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dunit">dunit</a></span> =&gt; "<span class="id">unit</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dnat">dnat</a></span> <span class="id">z</span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Digits.html#Z_to_string10">Z_to_string10</a></span> <span class="id">z</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dfloat">dfloat</a></span> <span class="id">f</span> =&gt; <span class="id">to_string</span> <span class="id">f</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dbool">dbool</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#true">true</a></span> =&gt; "<span class="id">true</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dbool">dbool</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#false">false</a></span> =&gt; "<span class="id">false</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dstring">dstring</a></span> <span class="id">s</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#jsonify">jsonify</a></span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dstring">dstring</a></span> <span class="id">s</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dcoll">dcoll</a></span> <span class="id">arr</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"["<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#concat">String.concat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;", "<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">map</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_data">string_of_data</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span>) <span class="id">arr</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "]"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dleft">dleft</a></span> <span class="id">s</span> =&gt; "<span class="id">some</span>(" ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_data">string_of_data</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">s</span>) ++ ")"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dright">dright</a></span> <span class="id">_</span> =&gt; "<span class="id">none</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dbrand">dbrand</a></span> (<span class="id">b</span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>) <span class="id">d</span>' =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#print_brand">print_brand</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">b</span> ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_data">string_of_data</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">d</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dbrand">dbrand</a></span> <span class="id">_</span> <span class="id">_</span> =&gt; "???<span class="id">more</span> <span class="id">than</span> <span class="id">one</span> <span class="id">brand</span>???"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#drec">drec</a></span> <span class="id">r</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_rec">string_of_rec</a></span> <span class="id">r</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dforeign">dforeign</a></span> (<span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#enhanceddateTime">ErgoEnhancedModel.enhanceddateTime</a></span> <span class="id">dt</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">dateTime</span>(""" ++ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_to_string">DateTimeModelPart.DATE_TIME_to_string</a></span> <span class="id">dt</span> ++ """)"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dforeign">dforeign</a></span> (<span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#enhanceddateTimeinterval">ErgoEnhancedModel.enhanceddateTimeinterval</a></span> <span class="id">dti</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">duration</span>(" ++ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION_to_string">DateTimeModelPart.DATE_TIME_DURATION_to_string</a></span> <span class="id">dti</span> ++ ")"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dforeign">dforeign</a></span> <span class="id">_</span> =&gt; "???<span class="id">UnknownForeign</span>???"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#PrintTypedData.Data">Data</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="kwd">Types</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Import</span> <span class="id">ErgoCTypes</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Context</span> {<span class="id">br</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.TBrandModel.html#brand_model">brand_model</a></span>}.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="rtype_to_string">rtype_to_string</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) (<span class="id">t</span> : <span class="id">rtype</span>₀) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#t">t</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Bottom</span>₀ =&gt; "<span class="id">Nothing</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Top</span>₀ =&gt; "<span class="id">Any</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Unit</span>₀ =&gt; "<span class="id">Unit</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Nat</span>₀ =&gt; "<span class="id">Integer</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Float</span>₀ =&gt; "<span class="id">Double</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Bool</span>₀ =&gt; "<span class="id">Boolean</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">String</span>₀ =&gt; "<span class="id">String</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Coll</span>₀ <span class="id">r</span>' =&gt; (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#rtype_to_string">rtype_to_string</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">r</span>') ++ "[]"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Rec</span>₀ <span class="id">k</span> <span class="id">srl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">recend</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id">k</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.RType.html#Closed">Closed</a></span> =&gt; ""<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="kwd">Open</span> =&gt; " .."<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"{" ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#concat">String.concat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(", ")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">map</a></span> (<span class="kwd">fun</span> <span class="id">sr</span> =&gt; ((<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#sr">sr</a></span>) ++ ": " ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#rtype_to_string">rtype_to_string</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#sr">sr</a></span>))))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">srl</span>)) ++ <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#recend">recend</a></span> ++ "}"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Either</span>₀ <span class="id">tl</span> <span class="id">tr</span> =&gt; (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#rtype_to_string">rtype_to_string</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">tl</span>) ++ "?"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Arrow</span>₀ <span class="id">tin</span> <span class="id">tout</span> =&gt; (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#rtype_to_string">rtype_to_string</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">tin</span>) ++ " -&gt; " ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#rtype_to_string">rtype_to_string</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">tout</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Brand</span>₀ (<span class="id">b</span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>) =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#print_brand">print_brand</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">b</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Brand</span>₀ <span class="id">_</span> =&gt; "~" ++ "[<span class="id">multiple</span>]"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Foreign</span>₀ <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#enhancedDateTime">ErgoEnhancedModel.enhancedDateTime</a></span> =&gt; "<span class="id">DateTime</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Foreign</span>₀ <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#enhancedDateTimeInterval">ErgoEnhancedModel.enhancedDateTimeInterval</a></span> =&gt; "<span class="id">Duration</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">Foreign</span>₀ <span class="id">_</span> =&gt; "(<span class="id">unknown</span> <span class="id">foreign</span> <span class="id">type</span>)"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergoc_type_to_string">ergoc_type_to_string</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) (<span class="id">t</span> : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ectype">ectype</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#rtype_to_string">rtype_to_string</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> (<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_unpack">ergoc_type_unpack</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#t">t</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="string_of_result_type">string_of_result_type</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) (<span class="id">result</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#result">result</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; ""<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">typ</span> =&gt; " : " ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">typ</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="unpack_error">unpack_error</a></span> <span class="id">nsctxt</span> <span class="id">kind</span> <span class="id">out</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;("<span class="id">Cannot</span> <span class="id">unpack</span> <span class="id">type</span>: "<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_result_type">string_of_result_type</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#out">out</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ " (<span class="id">expected</span> "<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++  <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#kind">kind</a></span> ++ ")").<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="unpack_failure_type">unpack_failure_type</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">out</span> : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">osuccess</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.unteither">unteither</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#out">out</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">tl</span>, <span class="id">tr</span>) =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">tl</span>, <span class="id">tr</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Lift.html#lift">lift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#osuccess">osuccess</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_error">unpack_error</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> "<span class="id">either</span>" <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#out">out</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="unpack_success_type">unpack_success_type</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">out</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> * <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> * <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">osuccess</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.unteither">unteither</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#out">out</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">tl</span>, <span class="id">tr</span>) =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">tl</span>, <span class="id">tr</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">success</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Lift.html#lift">lift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#osuccess">osuccess</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_error">unpack_error</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> "<span class="id">either</span>" <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#out">out</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">response</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">success</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span> (<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_infer_unary_op">ergoc_type_infer_unary_op</a></span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpDot">OpDot</a></span> "<span class="id">response</span>") <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#success">success</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_error">unpack_error</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> "<span class="id">response</span>" <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#out">out</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#success">success</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">emit</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">success</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span> (<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_infer_unary_op">ergoc_type_infer_unary_op</a></span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpDot">OpDot</a></span> "<span class="id">emit</span>") <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#success">success</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_error">unpack_error</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> "<span class="id">emit</span>" <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#out">out</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#success">success</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">state</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">success</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span> (<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_infer_unary_op">ergoc_type_infer_unary_op</a></span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpDot">OpDot</a></span> "<span class="id">state</span>") <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#success">success</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_error">unpack_error</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> "<span class="id">state</span>" <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#out">out</a></span>))) <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#success">success</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="kwd">fun</span> <span class="id">r</span> <span class="id">e</span> <span class="id">s</span> =&gt; (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#r">r</a></span>,<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#e">e</a></span>,<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#s">s</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#response">response</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#emit">emit</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#state">state</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="unpack_output_type">unpack_output_type</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">out</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> * <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> * <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> * <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">respt</span>,<span class="id">emitt</span>,<span class="id">statet</span>) := <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#x">x</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">respt</span>,<span class="id">emitt</span>,<span class="id">statet</span>,<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#y">y</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_success_type">unpack_success_type</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#out">out</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_failure_type">unpack_failure_type</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#out">out</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="kwd">Types</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="PrintTypedData.Both">Both</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Context</span> {<span class="id">br</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.TBrandModel.html#brand_model">brand_model</a></span>}.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="string_of_response">string_of_response</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">response</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">response_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">Response</span>. " ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_data">string_of_data</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#response">response</a></span>) ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_result_type">string_of_result_type</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#response_type">response_type</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="string_of_emits">string_of_emits</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">emits</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">emit_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#emits">emits</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> =&gt; ""<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">e1</span> :: <span class="id">erest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">new</span> <span class="id">old</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#old">old</a></span> ++ <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#fmt_nl">fmt_nl</a></span> ++ "<span class="id">Emit</span>. " ++ <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#new">new</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;("<span class="id">Emit</span>. " ++ <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_data">string_of_data</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">map</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_data">string_of_data</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span>) <span class="id">erest</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_result_type">string_of_result_type</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#emit_type">emit_type</a></span>) ++ <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#fmt_nl">fmt_nl</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="string_of_state">string_of_state</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">old_state</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">new_state</span> : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">state_type</span>: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">jsonify</span> := <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_data">string_of_data</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#old_state">old_state</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt;  <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#fmt_nl">fmt_nl</a></span> ++ "<span class="id">State</span>. " ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#jsonify">jsonify</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#new_state">new_state</a></span>) ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_result_type">string_of_result_type</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#state_type">state_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">actual_old_state</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#data_eq_dec">Data.data_eq_dec</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#new_state">new_state</a></span> <span class="id">actual_old_state</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> ""<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#fmt_nl">fmt_nl</a></span> ++ "<span class="id">State</span>. " ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#jsonify">jsonify</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#new_state">new_state</a></span>) ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_result_type">string_of_result_type</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#state_type">state_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="string_of_typed_data">string_of_typed_data</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">old_state</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">data</span>: <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">typ</span>: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#data">data</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dright">dright</a></span> <span class="id">msg</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">failure_type</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#typ">typ</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt;  <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">typ</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_failure_type">unpack_failure_type</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#typ">typ</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">f</span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">f</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">_</span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">Failure</span>. " ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_data">string_of_data</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">msg</span>) ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_result_type">string_of_result_type</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#failure_type">failure_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">out</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_output">unpack_output</a></span> <span class="id">out</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">response</span>, <span class="id">emits</span>, <span class="id">state</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">response_type</span>, <span class="id">emit_type</span>, <span class="id">state_type</span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#typ">typ</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt;  (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">typ</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_success_type">unpack_success_type</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#typ">typ</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> (<span class="id">r</span>,<span class="id">e</span>,<span class="id">s</span>) =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">r</span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">e</span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">s</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">_</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_emits">string_of_emits</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">emits</span> <span class="id">emit_type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_response">string_of_response</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">response</span> <span class="id">response_type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_state">string_of_state</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#old_state">old_state</a></span> <span class="id">state</span> <span class="id">state_type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_data">string_of_data</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id">out</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="string_of_typed_result">string_of_typed_result</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">old_state</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">result</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergo_data">ergo_data</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#result">result</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id">_</span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>) =&gt; ""<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id">typ</span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">dat</span>) =&gt; (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#string_of_typed_data">string_of_typed_data</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#old_state">old_state</a></span> <span class="id">dat</span> <span class="id">typ</span>) ++ <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#fmt_nl">fmt_nl</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#PrintTypedData.Both">Both</a></span>.<br/>
<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#PrintTypedData">PrintTypedData</a></span>.<br/>
<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
